COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	#. %3Prioritized circumscription%1
C00008 ENDMK
C⊗;
#. %3Prioritized circumscription%1

	An alternate way of introducing formula circumscription is by
means of an ordering formulas involving
tuples of predicates satisfying an axiom.  We write ⊗E(P)
for ⊗λx.E(P,x) and define %2E(P)_≤_E(P')%1 by

!!k10:	%2∀P P'.E(P) ≤ E(P') ≡ ∀x.E(P,x) ⊃ E(P',x)%1.

That ⊗E(P0) is a relative minimum in this ordering is expressed by

!!k11:	%2∀P.E(P) ≤ E(P0) ⊃ E(P) = E(P0)%1,

where equality is interpreted extensionally, i.e. we have

!!k12:	%2∀P P'.E(P) = E(P') ≡ (∀x.E(P,x) ≡ E(P',x))%1.

Assuming that we look for a minimum among predicates ⊗P satisfying ⊗A(P), 
then ({eq k10}) expands to precisely to the circumscription formula ({eq a1}).
In some earlier expositions of circumscription this ordering
approach was used, and Vladimir Lifschitz in a recent seminar advocated
returning to it as a more fundamental and understandable concept.

	I'm beginning to think he's right about it being more
understandable, but there seems to be a more fundamental reason for using
it.  Namely, certain common sense axiomatizations are easier to formalize
if we use a new kind of ordering, and circumscription based on this kind
of ordering doesn't seem to reduce to ordinary formula circumscription.

	We call it %3prioritized circumscription%1.

	Suppose we write some bird axioms in the form

!!k1:	%2∀x.¬ab aspect1 x ⊃ ¬flies x%1

and

!!k2:	%2∀x.bird x ∧ ¬ab aspect2 x ⊃ ab aspect1 x%1.

	The intent is clear.  The goal is that being a bird and
not abnormal in ⊗aspect2 prevents
the application of ({eq k1}).  However, circumscribing ⊗ab_z with
the conjunction of ({eq k1}) and ({eq k2}) as ⊗A(ab) doesn't have this effect,
because ({eq k2}) is equivalent to

!!k3:	%2∀x.bird x ⊃ ab aspect1 x ∨ ab aspect2 x%1,

and there is no indication that one would prefer to have
⊗aspect1_x abnormal than to have ⊗aspect2_x abnormal.  Circumscription
then results in a disjunction which is not wanted in this case.
The need to avoid this disjunction is
why the axioms were written as they are in section 4.  Namely,

	%2∀x.bird x ⊃ ab aspect1 x%1

avoided the disjunction

	However, by using a new kind of ordering we can leave ({eq k1}) and
({eq k2}) as is, and still get the desired effect.

	We define two orderings on ⊗ab predicates, namely

!!k4:	%2∀ab ab'.ab ≤q1 ab' ≡ ∀x.ab aspect1 x ⊃ ab' aspect1 x%1

and

!!k5:	%2∀ab ab'.ab ≤q2 ab' ≡ ∀x.ab aspect2 x ⊃ ab' aspect2 x%1.

We then combine these orderings lexicographically giving %2≤q2%1
priority over %2≤q1%1 getting

!!k6:	%2∀ab ab'.ab ≤%41<2%* ab' ≡ ab ≤q2 ab' ∨ ab =q2 ab' ∧ ab ≤q1 ab'%1.

	Choosing ⊗ab0 so as to minimize this ordering yields the
result that exactly birds can fly.  However, if we add

!!k7:	%2∀x.ostrich x ⊃ ab aspect2 x%1,

we'll get that ostriches (whether or not ostriches are birds)
don't fly without further axioms.  If we use

!!k8:	%2∀x.ostrich x ∧ ¬ab aspect3 x ⊃ ab aspect2 x%1

instead of ({eq k7}), we'll have to revise our notion of ordering
to put minimizing %2ab_aspect3_x%1 at higher priority than minimizing
⊗aspect2_x and %2a fortiori%1 at higher priority than minimizing
⊗aspect1. 

	This suggests providing a partial ordering on aspects
giving their priorities and providing axioms that permit deducing
the ordering on ⊗ab from the sentences that describe the ordering
relations.  We haven't been able to work this out yet.  It would
apparently be a considerable elaboration of the formalism.

	I am hopeful that some version of %2prioritized circumscription%1
will turn out to be the most natural and powerful variant.

.skip 2